A:Type, B, C:(AType), eq:EqDecider(A), f:a:A fp B(a), g:a:A fp C(a).
(x:A. ((x  dom(f)) & (x  dom(g)))  ((B(x) r C(x)) c (f(x) = g(x)  C(x))))
 g  f  g 

latex

Definitions	x:A. B(x), x(s), P  Q, P & Q, A c B, f  g, t  T, , x. t(x), P  Q, {T}, f(x), f  g, t.2, f(x)?z, if b then t else f fi , tt, ff, P  Q, P  Q, , Unit,
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, fpf wf, deq wf, fpf-join-dom2, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot